FDL - Nuprl Lemma : es-first-at-since-iff

Nuprl Lemma : es-first-at-since-iff

es:ES, i:Id, e:E, P, R:({e:E| loc(e) = i}

).
(

e:E. (loc(e) = i)

Dec(R(e)))

(es-first-at-since(es;i;e;e.R(e);e.P(e))

((loc(e) = i)

c

(P(e) & (

R(e))

c

& ((

e'':E. ((e'' <loc e) c

P(e'')))

c

& (

(

e':E

c

& (

(

((e' <loc e)

c

& (

(

c

(R(e')

c

& (

(

c

& (

e'':E.

c

& (

(

c

& ((e' <loc e'')

(e'' <loc e)

((

P(e'')) & (

R(e'')))))))))))

Definitions x:A. B(x), , P Q, x(s), P Q, A c B, P & Q, x:A. B(x), (e <loc e'), P Q, t T, x. t(x), es-first-at-since(es;i;e;e.R(e);e.P(e)), e<e'. P(e), e loc e' , P Q, A, False

Lemmas Id wf, es-loc wf, es-causl wf, es-loc-pred, es-locl-iff, es-first-at-since wf, not wf, es-E wf, decidable wf, event system wf, es-locl wf, es-le-loc, es-le-not-locl